#!/bin/bash

#File = simple_sum.cnf
#Variables = 183
#Clauses = 556
#Status = SAT
#Block = 8
#Thread = 1
#Jobs = 64
#Average = 5.50000
#Count = 1
#File = simple_sum.cnf
#Variables = 183
#Clauses = 556
#Status = SAT
#Block = 16
#Thread = 1
#Jobs = 64
#Average = 6.38000
#Count = 1

while read line
do

	if [[ "$line" =~ "File = " ]] || [[ "$line" =~ "Variables = " ]] || [[ "$line" =~ "Clauses = " ]] || [[ "$line" =~ "Status = " ]] || [[ "$line" =~ "Block = " ]] || [[ "$line" =~ "Thread = " ]] || [[ "$line" =~ "Jobs = " ]] || [[ "$line" =~ "Average = " ]] || [[ "$line" =~ "Count = " ]]
	then
		CONTENT=`echo "$line" | cut -d " " -f 3`
		echo -n $CONTENT

		if [[ "$line" =~ "Count = " ]]
		then
			echo
		else
			echo -n ","
		fi

		if [[ "$line" =~ "Average = " ]]
		then
			echo -n ",,"
		fi
	fi


done
